M:MsgA, x:Id. Dec(x declared in M) 

latex

Definitions	Id, t  T, x:A. B(x), x. t(x), Top, a:A fp B(a), IdDeq, x  dom(f), b, Dec(P), x declared in M, MsgA
Lemmas	msga wf, decidable assert, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, Id wf